(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 3))
(let ((e4 6))
(let ((e5 (- v2)))
(let ((e6 (- e5 v1)))
(let ((e7 (- e6 v0)))
(let ((e8 (+ e7 e7)))
(let ((e9 (/ e4 (- e3))))
(let ((e10 (distinct e8 v2)))
(let ((e11 (< e8 v0)))
(let ((e12 (< e7 e8)))
(let ((e13 (< v0 e8)))
(let ((e14 (< v2 e7)))
(let ((e15 (< v0 e7)))
(let ((e16 (> e7 e9)))
(let ((e17 (= e7 e5)))
(let ((e18 (>= e8 v1)))
(let ((e19 (distinct e7 e8)))
(let ((e20 (>= e5 e5)))
(let ((e21 (= e7 e5)))
(let ((e22 (> e7 e5)))
(let ((e23 (= e8 v0)))
(let ((e24 (< e6 v2)))
(let ((e25 (> e5 v0)))
(let ((e26 (< e8 e9)))
(let ((e27 (> e5 e7)))
(let ((e28 (distinct v0 e9)))
(let ((e29 (= e6 v2)))
(let ((e30 (distinct e7 e9)))
(let ((e31 (distinct e5 v0)))
(let ((e32 (< e7 e7)))
(let ((e33 (> e5 e6)))
(let ((e34 (<= e8 v2)))
(let ((e35 (distinct e6 e8)))
(let ((e36 (< e8 v2)))
(let ((e37 (distinct v1 v0)))
(let ((e38 (xor e20 e25)))
(let ((e39 (or e22 e17)))
(let ((e40 (and e26 e35)))
(let ((e41 (=> e28 e10)))
(let ((e42 (ite e38 e15 e31)))
(let ((e43 (xor e21 e21)))
(let ((e44 (and e24 e43)))
(let ((e45 (ite e37 e29 e37)))
(let ((e46 (or e40 e36)))
(let ((e47 (or e13 e46)))
(let ((e48 (xor e47 e33)))
(let ((e49 (=> e14 e12)))
(let ((e50 (not e41)))
(let ((e51 (xor e45 e32)))
(let ((e52 (xor e23 e18)))
(let ((e53 (=> e16 e49)))
(let ((e54 (ite e50 e11 e44)))
(let ((e55 (xor e51 e51)))
(let ((e56 (or e30 e42)))
(let ((e57 (not e48)))
(let ((e58 (xor e34 e55)))
(let ((e59 (not e57)))
(let ((e60 (= e58 e19)))
(let ((e61 (not e53)))
(let ((e62 (and e54 e59)))
(let ((e63 (xor e61 e27)))
(let ((e64 (not e52)))
(let ((e65 (and e56 e56)))
(let ((e66 (or e39 e65)))
(let ((e67 (=> e64 e66)))
(let ((e68 (xor e67 e60)))
(let ((e69 (=> e63 e63)))
(let ((e70 (= e69 e62)))
(let ((e71 (=> e68 e68)))
(let ((e72 (xor e71 e70)))
e72
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
